1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
use super::*;
mod slice;
mod vec;
mod down;
pub use slice::*;
pub use vec::*;
pub use down::*;
pub trait SubstCtx {
type Ctx: TyCtxMut;
#[inline]
fn cache(&mut self, _term: &TermId, _subst: Option<&TermId>) -> Result<(), Error> {
Ok(())
}
#[inline]
fn try_subst(&mut self, _term: &Term) -> Option<Result<Option<TermId>, Error>> {
None
}
fn subst_constrain(
&mut self,
ix: u32,
annot: Option<&TermId>,
) -> Result<Option<TermId>, Error> {
if let Some(annot) = annot {
if let Some(false) = self.ctx().constrain(ix, annot)? {
return Err(Error::TypeMismatch);
}
}
self.subst_var(ix, annot)
}
fn subst_var(&mut self, ix: u32, annot: Option<&TermId>) -> Result<Option<TermId>, Error>;
fn push_param(&mut self, param_ty: Option<&TermId>) -> Result<Option<TermId>, Error>;
fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool;
fn ctx(&mut self) -> &mut Self::Ctx;
#[inline]
fn cons_ctx(&mut self) -> &mut <Self::Ctx as TyCtxMut>::ConsCtx {
self.ctx().cons_ctx()
}
#[inline]
fn eq_ctx(&mut self) -> &mut <Self::Ctx as TyCtxMut>::TermEqCtx {
self.ctx().eq_ctx()
}
#[inline]
fn push_param_ctx(&mut self, param_ty: Option<&TermId>) -> Result<(), Error> {
self.ctx().push_param(param_ty)
}
fn pop_param(&mut self) -> Result<(), Error>;
fn is_var_null(&self) -> bool;
}
pub trait EvalCtx: SubstCtx {
fn push_subst(&mut self, subst: TermId) -> Result<(), Error>;
fn pop_subst(&mut self) -> Result<(), Error>;
}